|
|
Detekce kompletnosti instrukční sady pro generování univerzálního překladače jazyka C
Nagy, Michal ; Dolíhal, Luděk (oponent) ; Hruška, Tomáš (vedoucí práce)
Práce se zabývá problematikou detekce kompletnosti popisu instrukční sady mikroprocesoru pro překladač LLVM, neboli schopností překladače vygenerovat cílový program pro každý validní zdrojový program v příslušném vyšším programovacím jazyce. Na základech teorie regulárních stromových gramatik a několika vědeckých prací, které se touto problematikou též zabývají, je navržen a implementován formální prostředek pro ověření inkluze dvou gramatik. Dále je navržen způsob automatické extrakce obou gramatik z popisu instrukční sady, v důsledku čehož je tento prostředek možné použít pro ověření kompletnosti výběru instrukcí. V kombinaci s ověřením kompletnosti tzv. procesu legalizace překladače LLVM, který výběr instrukcí předchází, by mělo být proveditelné ověření kompletnosti většiny části překladače závislých na popisu cílové architektury.
|
|
|
Classification of (in)finitary logics
Lávička, Tomáš ; Noguera, Carles (vedoucí práce) ; Botur, Michal (oponent)
V této magisterské práci se budeme zabývat větami o úplnosti v rámci abstraktní algebraické logiky. Náš ústřední zájem bude spočívat v úplnosti vůči takzvaným relativně (konečně) subdirektně ireducibilním modelům. Významnou úlohu popi- sované teorie hraje rozdíl mezi finitarními a infinitárními logickými systémy. Zaměříme se na dobře známý fakt, že pro každou finitární logiku lze dokázat větu o úplnosti vůči svým relativně (konečně) subdirektně ireducibilním modelům, a budeme se zabývat možností zobecnit tuto větu na logiky infinitární. Ukážeme, že existují dvě zajímavé vlastnosti, které leží mezi finitaritou a touto větou o úplnosti, jedná se o vlastnosti rozšíření na (úplně) průsekové prvoteorie. Na základě těchto pojmů zadefinujeme pět tříd logik a navrhneme novou hierarchy finitárních a infinitárních logik. Hlavním přínosem této práce je důkaz, že exis- tuje logika oddělující některé z těchto tříd. Klíčová slova: Abstraktní algebraická logika, úplnost, relativně (konečně) subdirektně ireducibilní modely, RSI-úplnost, RFSI-úplnost, vlastnost rozšíření na (úplně) průsekové prvoteorie, IPEP, CIPEP.
|
|
|
Detekce kompletnosti instrukční sady pro generování univerzálního překladače jazyka C
Nagy, Michal ; Dolíhal, Luděk (oponent) ; Hruška, Tomáš (vedoucí práce)
Práce se zabývá problematikou detekce kompletnosti popisu instrukční sady mikroprocesoru pro překladač LLVM, neboli schopností překladače vygenerovat cílový program pro každý validní zdrojový program v příslušném vyšším programovacím jazyce. Na základech teorie regulárních stromových gramatik a několika vědeckých prací, které se touto problematikou též zabývají, je navržen a implementován formální prostředek pro ověření inkluze dvou gramatik. Dále je navržen způsob automatické extrakce obou gramatik z popisu instrukční sady, v důsledku čehož je tento prostředek možné použít pro ověření kompletnosti výběru instrukcí. V kombinaci s ověřením kompletnosti tzv. procesu legalizace překladače LLVM, který výběr instrukcí předchází, by mělo být proveditelné ověření kompletnosti většiny části překladače závislých na popisu cílové architektury.
|
host ::
RSS.